Matches in value-assignements (V): {{numOfValueMatches}}
Matches in edge-description: {{numOfDescriptionMatches}}
Rank |
Scope |
|||
-V- |
{{line.bestrank}}
|
{{line.desc}}
|
| Precondition (initial variable assignment): |
|
{{precondition}} |
| {{fault.rank}}. | {{fault.score}} | Details: | ||||
Current values:
|
||||||
1 | //#include <stdio.h> |
2 | //#include <stdlib.h> |
3 | //#include <assert.h> |
4 | |
5 | // Structure to hold division result |
6 | //typedef struct { |
7 | // int quotient; |
8 | // int remainder; |
9 | //} DivisionResult; |
10 | |
11 | // Function prototypes |
12 | |
13 | // Arithmetic class implementation |
14 | int add(int a, int b) { |
15 | //assert(a >= -100 && a <= 100); |
16 | //assert(b >= -100 && b <= 100); |
17 | |
18 | int i, result; |
19 | |
20 | if (b >= 0) { |
21 | //printf("branch 2\n"); |
22 | result = a; |
23 | i = b; |
24 | while (i != 0) { |
25 | result = result + 1; |
26 | i = i - 1; |
27 | } |
28 | } else { |
29 | //printf("branch 3\n"); |
30 | result = a; |
31 | i = b; |
32 | while (i != 0) { |
33 | result = result - 1; |
34 | i = i + 1; |
35 | } |
36 | } |
37 | return result; |
38 | } |
39 | |
40 | int add_recursive(int a, int b) { |
41 | //assert(a >= -100 && a <= 100); |
42 | //assert(b >= -100 && b <= 100); |
43 | |
44 | int result; |
45 | if (b == 0) { |
46 | //printf("branch 4\n"); |
47 | result = a; |
48 | } else if (b > 0) { |
49 | //printf("branch 5\n"); |
50 | result = add_recursive(a, b - 1) + 1; |
51 | } else { |
52 | //printf("branch 6\n"); |
53 | result = add_recursive(a, b + 1) - 1; |
54 | } |
55 | return result; |
56 | } |
57 | |
58 | int multiply(int a, int b) { |
59 | //assert(a >= -10 && a <= 10); |
60 | //assert(b >= 0 && b <= 10); |
61 | int i, result; |
62 | if (a == 0 || b == 0) { |
63 | //printf("branch 7\n"); |
64 | result = 0; |
65 | } else { |
66 | //printf("branch 8\n"); |
67 | result = a; |
68 | i = b; |
69 | while (i != 1) { |
70 | result = add(result, a); |
71 | i = i - 1; |
72 | } |
73 | } |
74 | return result; |
75 | } |
76 | |
77 | int multiply_recursive(int a, int b) { |
78 | //assert(a >= -10 && a <= 10); |
79 | //assert(b >= 0 && b <= 10); |
80 | int result; |
81 | |
82 | if (a == 0 || b == 0) { |
83 | //printf("branch 9\n"); |
84 | result = 0; |
85 | } else { |
86 | if (b == 1) { |
87 | // printf("branch 10\n"); |
88 | result = a; |
89 | } else { |
90 | //printf("branch 11\n"); |
91 | result = add_recursive(a, multiply(a, b - 1)); |
92 | } |
93 | } |
94 | return result; |
95 | } |
96 | |
97 | int divide(int n, int m) { |
98 | //assert(n >= 0); |
99 | //assert(m > 0); |
100 | //assert(n <= 100 && m <= 100); |
101 | |
102 | int q, r; |
103 | |
104 | r = n; |
105 | q = 0; |
106 | |
107 | while (r >= m) { |
108 | //printf("branch 12\n"); |
109 | r = add(r, -m); |
110 | q = q + 1; |
111 | } |
112 | |
113 | int result_1 = q; |
114 | int result_2 = r; |
115 | //{q, r}; |
116 | return result_1; |
117 | } |
118 | |
119 | int divide_recursive(int n, int m) { |
120 | //assert(n >= 0); |
121 | //assert(m > 0); |
122 | //assert(n <= 100 && m <= 100); |
123 | |
124 | int result_quotient, result_remainder; |
125 | int res_remainder, res_quotient; |
126 | |
127 | if (n < m) { |
128 | //printf("branch 13\n"); |
129 | result_quotient = 0; |
130 | result_remainder = n; |
131 | } else { |
132 | //printf("branch 14\n"); |
133 | res_quotient = divide_recursive(add_recursive(n, -m), m); |
134 | result_quotient = res_quotient + 1; |
135 | result_remainder = res_remainder; |
136 | } |
137 | |
138 | return result_quotient; |
139 | } |
140 | |
141 | // Main function for testing |
142 | int main() { |
143 | // Test add |
144 | //printf("Add: %d\n", add(5, 3)); |
145 | |
146 | // Test add_recursive |
147 | //printf("Add recursive: %d\n", add_recursive(5, 3)); |
148 | |
149 | // Test multiply |
150 | //printf("Multiply: %d\n", multiply(5, 3)); |
151 | |
152 | // Test multiply_recursive |
153 | //printf("Multiply recursive: %d\n", multiply_recursive(5, 3)); |
154 | |
155 | // Test divide |
156 | //int div_result = divide(10, 3); |
157 | //printf("Divide: quotient = %d, remainder = %d\n", div_result.quotient, div_result.remainder); |
158 | |
159 | // Test divide_recursive |
160 | //int div_result_rec = divide_recursive(10, 3); |
161 | //printf("Divide recursive: quotient = %d, remainder = %d\n", div_result_rec.quotient, div_result_rec.remainder); |
162 | |
163 | int n, m; |
164 | int a, b; |
165 | |
166 | add (a, b); |
167 | add_recursive (a, b); |
168 | |
169 | multiply(a, b); |
170 | multiply_recursive(a, b); |
171 | |
172 | divide (n, m); |
173 | divide_recursive (n, m); |
174 | |
175 | return 0; |
176 | } |
177 |
| Date | Time | Level | Component | Message |
|---|---|---|---|---|
| 2024-08-21 | 20:22:47:018 | INFO | CPAMain.detectFrontendLanguageIfNecessary | Language C detected and set for analysis |
| 2024-08-21 | 20:22:47:048 | INFO | ResourceLimitChecker.fromConfiguration | Using the following resource limits: CPU-time limit of 900s |
| 2024-08-21 | 20:22:47:111 | INFO | CPAchecker.run | CPAchecker 3.0 / testCaseGeneration-bmc (Java HotSpot(TM) 64-Bit Server VM 20.0.2) started |
| 2024-08-21 | 20:22:47:126 | INFO | CPAchecker.parse | Parsing CFA from file(s) "doc/examples/arithmetic_2.c" |
| 2024-08-21 | 20:22:47:881 | INFO | PredicateCPA PredicateCPA.<init> | Using predicate analysis with MathSAT5 version 5.6.10 (953b604e7ca7) (May 31 2023 12:36:26, gmp 6.0.0/mpir 3.0.0, msvc 19.12, 64-bit). |
| 2024-08-21 | 20:22:48:191 | WARNING | CPAchecker.printConfigurationWarnings | The following configuration options were specified but are not used: cpa.automaton.breakOnTargetState |
| 2024-08-21 | 20:22:48:191 | INFO | CPAchecker.runAlgorithm | Starting analysis ... |
| 2024-08-21 | 20:22:48:202 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:261 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:262 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:295 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:297 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:298 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:308 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:317 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:318 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:327 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:329 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:330 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:331 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:337 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:338 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:348 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:350 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:351 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:360 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:373 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:373 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:388 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:390 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:390 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:391 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:397 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:397 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:408 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:409 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:410 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:421 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:424 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:424 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:435 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:440 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:440 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:442 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:446 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:448 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:462 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:463 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:466 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:480 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:484 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:486 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:499 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:501 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:504 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:505 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:511 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:515 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:531 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:533 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:537 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:552 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:558 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:559 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:563 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 2 |
| 2024-08-21 | 20:22:48:563 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:567 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:571 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:585 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:616 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:620 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:634 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:638 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:642 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:656 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 3 |
| 2024-08-21 | 20:22:48:657 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:740 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:741 | INFO | AbstractBMCAlgorithm.analyzeCounterexample0 | Error found, creating error path |
| 2024-08-21 | 20:22:48:749 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:755 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:756 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:781 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 4 |
| 2024-08-21 | 20:22:48:782 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:806 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:807 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:831 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 5 |
| 2024-08-21 | 20:22:48:832 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:852 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:854 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:879 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 6 |
| 2024-08-21 | 20:22:48:880 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:900 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:901 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:928 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 7 |
| 2024-08-21 | 20:22:48:928 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:48:949 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:48:951 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:48:981 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 8 |
| 2024-08-21 | 20:22:48:982 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:002 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:003 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:035 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 9 |
| 2024-08-21 | 20:22:49:036 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:053 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:054 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:091 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 10 |
| 2024-08-21 | 20:22:49:092 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:108 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:109 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:145 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 11 |
| 2024-08-21 | 20:22:49:145 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:163 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:164 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:200 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 12 |
| 2024-08-21 | 20:22:49:201 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:217 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:219 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:260 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 13 |
| 2024-08-21 | 20:22:49:261 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:276 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:278 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:317 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 14 |
| 2024-08-21 | 20:22:49:317 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:336 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:338 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:391 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 15 |
| 2024-08-21 | 20:22:49:391 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:407 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:409 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:449 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 16 |
| 2024-08-21 | 20:22:49:450 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:465 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:466 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:508 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 17 |
| 2024-08-21 | 20:22:49:509 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:524 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:526 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:572 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 18 |
| 2024-08-21 | 20:22:49:573 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:587 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:589 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:636 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 19 |
| 2024-08-21 | 20:22:49:637 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:653 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:656 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:708 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 20 |
| 2024-08-21 | 20:22:49:708 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:726 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:728 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:784 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 21 |
| 2024-08-21 | 20:22:49:784 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:807 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:809 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:884 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 22 |
| 2024-08-21 | 20:22:49:884 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:899 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:902 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:49:953 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 23 |
| 2024-08-21 | 20:22:49:954 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:49:968 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:49:970 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:034 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 24 |
| 2024-08-21 | 20:22:50:035 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:50:050 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:50:052 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:109 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 25 |
| 2024-08-21 | 20:22:50:109 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:50:125 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:50:127 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:180 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 26 |
| 2024-08-21 | 20:22:50:181 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:50:194 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:50:197 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:258 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 27 |
| 2024-08-21 | 20:22:50:258 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:50:277 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:50:280 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:342 | INFO | LoopBoundCPA LoopBoundPrecisionAdjustment.nextState | Adjusting maxLoopIterations to 28 |
| 2024-08-21 | 20:22:50:342 | INFO | AbstractBMCAlgorithm.run | Creating formula for program |
| 2024-08-21 | 20:22:50:358 | INFO | AbstractBMCAlgorithm.boundedModelCheck | Starting satisfiability check... |
| 2024-08-21 | 20:22:50:361 | INFO | AbstractBMCAlgorithm.checkBoundingAssertions | Starting assertions check... |
| 2024-08-21 | 20:22:50:405 | WARNING | ForceTerminationOnShutdown$1.shutdownRequested | Shutdown requested (The JVM is shutting down, probably because Ctrl+C was pressed.), waiting for termination. |
| 2024-08-21 | 20:22:50:448 | SEVERE | TestCaseGeneratorAlgorithm.run | 17 of 26 covered |
| 2024-08-21 | 20:22:50:448 | WARNING | ShutdownNotifier.shutdownIfNecessary | Warning: Analysis interrupted (The JVM is shutting down, probably because Ctrl+C was pressed.) |
| Statistics Name | Statistics Value | Additional Value |
|---|---|---|
| PredicateCPA statistics | ||
| Number of abstractions | 49 | 1% of all post computations |
| Times abstraction was reused | 0 | |
| Because of function entry/exit | 0 | 0% |
| Because of loop head | 0 | 0% |
| Because of join nodes | 0 | 0% |
| Because of threshold | 0 | 0% |
| Because of target state | 49 | 100% |
| Times precision was empty | 49 | 100% |
| Times precision was {false} | 0 | 0% |
| Times result was cached | 0 | 0% |
| Times cartesian abs was used | 0 | 0% |
| Times boolean abs was used | 0 | 0% |
| Times result was 'false' | 0 | 0% |
| Number of strengthen sat checks | 0 | |
| Number of coverage checks | 614 | |
| BDD entailment checks | 0 | |
| Number of SMT sat checks | 0 | |
| trivial | 0 | |
| cached | 0 | |
| Max ABE block size | 46 | |
| Avg ABE block size | 21.41 | sum: 1049, count: 49, min: 8, max: 46 |
| Number of predicates discovered | 0 | |
| Time for post operator | 0.236s | |
| Time for path formula creation | 0.232s | |
| Time for strengthen operator | 0.004s | |
| Time for prec operator | 0.013s | |
| Time for abstraction | 0.002s | Max: 0.001s, Count: 49 |
| Solving time | 0.000s | Max: 0.000s |
| Model enumeration time | 0.000s | |
| Time for BDD construction | 0.000s | Max: 0.000s |
| Time for merge operator | 0.009s | |
| Time for coverage checks | 0.001s | |
| Total time for SMT solver (w/o itp) | 0.000s | |
| Total number of created targets for pointer analysis | 0 | |
| KeyValue statistics | ||
| Init. function predicates | 0 | |
| Init. global predicates | 0 | |
| Init. location predicates | 0 | |
| Invariant Generation statistics | ||
| Bounds CPA statistics | ||
| Bound k | 28 | |
| Maximum loop iteration reached | 29 | |
| ValueAnalysisCPA statistics | ||
| Number of variables per state | 1.23 | sum: 6832, count: 5552, min: 0, max: 2 |
| Number of global variables per state | 0.00 | sum: 0, count: 5552, min: 0, max: 0 |
| Number of assumptions | 1528 | |
| Number of deterministic assumptions | 0 | |
| Level of Determinism | 0% | |
| ValueAnalysisPrecisionAdjustment statistics | ||
| Number of abstraction computations | 6608 | |
| Total time for liveness abstraction | 0.000s | |
| Total time for abstraction computation | 0.003s | |
| Total time for path thresholds | 0.000s | |
| ConstraintsStrengthenOperator statistics | ||
| Total time for strengthening by ConstraintsCPA | 0.000s | |
| Replaced symbolic expressions | 0 | |
| CPA algorithm statistics | ||
| Number of iterations | 6614 | |
| Max size of waitlist | 437 | |
| Average size of waitlist | 219 | |
| LoopstackSortedWaitlist | 43.48 | sum: 6435, count: 148, min: 0, max: 233 |
| ReversePostorderSortedWaitlist | 20.07 | sum: 5619, count: 280, min: 0, max: 170 |
| LoopIterationSortedWaitlist | 42.59 | sum: 6303, count: 148, min: 0, max: 231 |
| CallstackSortedWaitlist | 1910.86 | sum: 93632, count: 49, min: 0, max: 6466 |
| Number of computed successors | 6644 | |
| Max successors for one state | 2 | |
| Number of times merged | 290 | |
| Number of times stopped | 297 | |
| Number of times breaked | 49 | |
| Total time for CPA algorithm | 0.558s | Max: 0.083s |
| Time for choose from waitlist | 0.008s | |
| Time for precision adjustment | 0.067s | |
| Time for transfer relation | 0.394s | |
| Time for merge operator | 0.025s | |
| Time for stop operator | 0.016s | |
| Time for adding to reached set | 0.012s | |
| BMC algorithm statistics | ||
| Time for BMC formula creation | 0.602s | |
| Time for final sat check | 0.041s | |
| Time for error-path creation | 0.020s | |
| Time for error-path post-processing | 0.165s | |
| Time for bounding assertions check | 1.147s | |
| Testtargets statistics | ||
| Test target coverage | 65.38% | |
| Number of total original test targets | 26 | |
| Number of total test targets | 26 | |
| Number of covered test targets | 17 | |
| Number of uncovered test targets | 9 | |
| Total time for test goal reduction | 0.000s | |
| Code Coverage | ||
| Function coverage | 1.000 | |
| Visited lines | 49 | |
| Total lines | 63 | |
| Line coverage | 0.778 | |
| Visited conditions | 17 | |
| Total conditions | 26 | |
| Condition coverage | 0.654 | |
| CPAchecker general statistics | ||
| Number of program locations | 122 | |
| Number of CFA edges (per node) | 142 | count: 122, min: 0, max: 5, avg: 1.16 |
| Number of relevant variables | 29 | |
| Number of functions | 7 | |
| Number of loops (and loop nodes) | 4 | sum: 16, min: 4, max: 4, avg: 4.00 |
| Size of reached set | 5552 | |
| Number of reached locations | 93 | 76% |
| Avg states per location | 59 | |
| Max states per location | 685 | at node N0 |
| Number of reached functions | 7 | 100% |
| Number of partitions | 5539 | |
| Avg size of partitions | 1 | |
| Max size of partitions | 5 (with key [N86 (before line 110), Function divide called from node N119, stack depth 2 [b25b095], stack [main, divide], ABS0: true, Undetermined loop iteration state; at least 3 iterations in some loop ({Loop with heads [N10] | |
| incoming | [line 24: N9 -{while}-> N10] | |
| outgoing | [line 24: N10 -{[! | i != 0]}-> N12] |
| nodes | [N10, N11, N13, N14] | |
| =3 through Loop with heads [N10] | ||
| incoming | [line 24: N9 -{while}-> N10] | |
| outgoing | [line 24: N10 -{[! | i != 0]}-> N12] |
| nodes | [N10, N11, N13, N14] | |
| , Loop with heads [N17] | ||
| incoming | [line 32: N16 -{while}-> N17] | |
| outgoing | [line 32: N17 -{[! | i != 0]}-> N19] |
| nodes | [N17, N18, N20, N21] | |
| =3 through Loop with heads [N17] | ||
| incoming | [line 32: N16 -{while}-> N17] | |
| outgoing | [line 32: N17 -{[! | i != 0]}-> N19] |
| nodes | [N17, N18, N20, N21] | |
| , Loop with heads [N83] | ||
| incoming | [line 107: N82 -{while}-> N83] | |
| outgoing | [line 107: N83 -{[! | r >= m]}-> N85] |
| nodes | [N83, N84, N86, N87] | |
| =3 through Loop with heads [N83] | ||
| incoming | [line 107: N82 -{while}-> N83] | |
| outgoing | [line 107: N83 -{[! | r >= m]}-> N85] |
| nodes | [N83, N84, N86, N87] | |
| })., stack depth 0 [2e0ad709]]) | ||
| Number of target states | 0 | |
| Size of final wait list | 400 | |
| Time for analysis setup | 1.065s | |
| Time for loading CPAs | 0.457s | |
| Time for loading parser | 0.136s | |
| Time for CFA construction | 0.423s | |
| Time for parsing file(s) | 0.197s | |
| Time for AST to CFA | 0.101s | |
| Time for CFA sanity check | 0.012s | |
| Time for post-processing | 0.082s | |
| Time for loop structure | 0.005s | |
| Time for AST structure | 0.000s | |
| Time for CFA export | 0.366s | |
| Time for function pointers resolving | 0.003s | |
| Function calls via function pointers | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer calls | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Function calls with function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Instrumented function pointer arguments | 0 | count: 1, min: 0, max: 0, avg: 0.00 |
| Time for classifying variables | 0.050s | |
| Time for collecting variables | 0.022s | |
| Time for solving dependencies | 0.001s | |
| Time for building hierarchy | 0.000s | |
| Time for building classification | 0.018s | |
| Time for exporting data | 0.009s | |
| Time for Analysis | 2.256s | |
| CPU time for analysis | 1.078s | |
| Total time for CPAchecker | 3.322s | |
| Total CPU time for CPAchecker | 1.313s | |
| Time for statistics | 0.113s | |
| Time for Garbage Collector | 0.039s | in 11 runs |
| Garbage Collector(s) used | G1 Concurrent GC, G1 Old Generation, G1 Young Generation | |
| Used heap memory | 49MB ( 47 MiB) max; 30MB ( 29 MiB) avg; 57MB ( 54 MiB) peak | |
| Used non-heap memory | 53MB ( 50 MiB) max; 42MB ( 40 MiB) avg; 54MB ( 51 MiB) peak | |
| Used in G1 Old Gen pool | 18MB ( 17 MiB) max; 12MB ( 12 MiB) avg; 18MB ( 17 MiB) peak | |
| Allocated heap memory | 532MB ( 508 MiB) max; 181MB ( 173 MiB) avg | |
| Allocated non-heap memory | 53MB ( 51 MiB) max; 44MB ( 42 MiB) avg | |
| Total process virtual memory | 689MB ( 657 MiB) max; 394MB ( 376 MiB) avg |
| # | Configuration Name | Configuration Value |
|---|---|---|
| 1 | analysis.algorithm.BMC | true |
| 2 | analysis.entryFunction | main |
| 3 | analysis.name | testCaseGeneration-bmc |
| 4 | analysis.programNames | doc/examples/arithmetic_2.c |
| 5 | analysis.traversal.order | bfs |
| 6 | analysis.traversal.useCallstack | true |
| 7 | analysis.traversal.useReverseLoopIterationCount | true |
| 8 | analysis.traversal.useReverseLoopstack | true |
| 9 | analysis.traversal.useReversePostorder | true |
| 10 | analysis.useTestCaseGeneratorAlgorithm | true |
| 11 | ARGCPA.cpa | cpa.composite.CompositeCPA |
| 12 | CompositeCPA.cpas | cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.functionpointer.FunctionPointerCPA, cpa.predicate.PredicateCPA, cpa.assumptions.storage.AssumptionStorageCPA, cpa.loopbound.LoopBoundCPA, cpa.value.ValueAnalysisCPA, cpa.testtargets.TestTargetCPA |
| 13 | cpa | cpa.arg.ARGCPA |
| 14 | cpa.arg.lateMerge | prevent |
| 15 | cpa.automaton.breakOnTargetState | 0 |
| 16 | cpa.composite.aggregateBasicBlocks | false |
| 17 | cpa.loopbound.maxLoopIterationAdjusterFactory | INCREMENT |
| 18 | cpa.loopbound.maxLoopIterations | 1 |
| 19 | cpa.loopbound.maxLoopIterationsUpperBound | 0 |
| 20 | cpa.predicate.blk.alwaysAtFunctions | false |
| 21 | cpa.predicate.blk.alwaysAtLoops | false |
| 22 | cpa.predicate.blk.useCache | false |
| 23 | cpa.predicate.ignoreIrrelevantVariables | false |
| 24 | cpa.predicate.invariants.export | false |
| 25 | cpa.predicate.invariants.exportAsPrecision | false |
| 26 | cpa.predicate.predmap.export | false |
| 27 | cpa.value.merge | JOIN |
| 28 | language | C |
| 29 | limits.time.cpu | 900s |
| 30 | log.level | INFO |
| 31 | specification | config/properties/coverage-branches.prp |
| 32 | testcase.targets.type | TEST_COMP_ASSUME |
This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.
License: Apache 2.0 License
Source: {{dependency.repository}}
{{dependency.copyright}}
License:
Full text of license
{{dependencies.licenses[dependency.licenseId]}}